COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Boyer and Moore lead the world's most successful group in automated theorem
C00003 ENDMK
C⊗;
Boyer and Moore lead the world's most successful group in automated theorem
proving and interactive theorem proving.  Their work gets closer all
the time to central problems of mathematical proof as well as to
central problems of program proving.

Their facilities and expertise in computer aided proof
and Chou's knowledge of geometry and experience with Wu's prover
combine to make the strongest possible attack on these problems.
This proposal is very strong both mathematically and computationally.
It should be supported as proposed.